i:Id, da:k:Knd fp Type, snd1, snd2:kl:KndIdLnk fp (IdTop) List.
snd1 || snd2
 (msg-spec-loc-decl(snd1  snd2;i;da)
 (
 (msg-spec-loc-decl(snd1;i;da) & msg-spec-loc-decl(snd2;i;da)) 

latex

Definitions

Top, t  T, Id, x:AB(x), x:A. B(x), x:AB(x), (x  l), b, P  Q, xL. P(x), Knd, Type, x.A(x), x. t(x), a:A fp B(a), rcv(l,tg), KindDeq, x  dom(f), Prop, <a,b>, IdLnkDeq, IdLnk, product-deq(A;B;a;b), type List, f(x), 1of(t), {T}, P  Q, left+right, P  Q, P & Q, P  Q, f  g, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, f || g, map(f;as), source(l), s = t, msg-spec-loc-decl(snd;i;da), a  b, , False, A, b, , Unit, Void, x:A. B(x), {x:A| B(x) }, ||as||, ij, a<b, AB, , , SQType(T), s ~ t, Atom$n, 2of(t), #$n, car.cdr, nil

Lemmas

bool cases, bool sq, le wf, cons one one, pi2 wf, Id sq, nat wf, non neg length, length wf1, member wf, l member wf, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, lsrc wf, l all wf, map wf, fpf-compatible wf, fpf wf, l all map, fpf-join wf, fpf-join-dom, pi1 wf, fpf-ap wf, product-deq wf, IdLnk wf, idlnk-deq wf, assert wf, fpf-dom wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf, Id wf, top wf